Quantified belief propagation has many applications, such as in the field of program synthesis, which involves discovering programs that realize specified user intent. Program synthesis can be useful in scenarios such as: enabling people with no programming background to develop utility programs, helping regular programmers automatically discover tricky or mundane details, program understanding, discovery of new algorithms, and even teaching. The program synthesis problem can be thought of as a search for a desired program over a given search space, starting from some given specification of user intent.
In several of the program synthesis examples listed above, the problem reduces to the problem of solving a QBF (Quantified Boolean Formulas) formula of the form ∃ x·∀ y·φ( x, y), where x and y are vectors of variables, and all the existential quantifiers in the formula occur before all the universal quantifiers. This naturally happens when the search space is that of straight-line programs, or the user specification is in the form of input-output examples. Recently, it was shown that even synthesis of loopy programs can be reduced to solving QBF formulas after some reduction involving the use of templates.
The class of straight-line programs, or more generally, loop-free programs, parameterized by the set of operators or components used, can often express a wide range of useful programs. Even though these types of programs may not involve loops, they can be challenging to synthesize. Moreover, the space of loop-free programs is vast and the number of possible programs is exponential in the number of components in the program. Brute-force search methods do not scale well for these problems.
There are two drawbacks in the current development approaches to solving program synthesis problems. First, most of the abovementioned program synthesis problems have necessitated development of new problem-specific algorithms. These algorithms are based on a variety of approaches ranging from exhaustive search, version space algebras, genetic programming, and SAT/SMT (Satisfaction/Satisfiability Modula Theories) solving. The second drawback is that these specialized algorithms do not scale well.
Described below are techniques to solve ∃*∀*QBF formulas (existentially and universally quantified QBF) using probabilistic inference techniques. While the techniques are useful for program synthesis, they have application beyond the program synthesis problem.